(agda2-status-action "")
(agda2-info-action "*Type-checking*" "" nil)
(agda2-highlight-clear)
(agda2-highlight-add-annotations 'nil '(1 7 (keyword) t) '(18 23 (keyword) t) '(25 29 (keyword) t) '(30 36 (keyword) t) '(50 70 (comment) t) '(74 75 (symbol) t) '(80 81 (symbol) t) '(90 91 (symbol) t))
(agda2-highlight-add-annotations 'nil '(1 7 (keyword) t) '(8 17 (module) nil nil ("Issue4260.agda" . 1)) '(18 23 (keyword) t) '(37 48 (module) nil nil ("Issue4260/M.agda" . 1)) '(72 73 (function) nil nil ("Issue4260.agda" . 72)) '(76 79 (primitive) nil nil ("agda-default-include-path/Agda/Primitive.agda" . 311)) '(82 85 (primitive) nil nil ("agda-default-include-path/Agda/Primitive.agda" . 311)) '(86 87 (function) nil nil ("Issue4260.agda" . 72)) '(88 89 (bound) nil nil ("Issue4260.agda" . 88)) '(92 93 (postulate) nil nil ("Issue4260/M.agda" . 39)) '(94 95 (bound) nil nil ("Issue4260.agda" . 88)))
(agda2-highlight-add-annotations 'nil '(25 29 (keyword) t) '(30 36 (keyword) t) '(37 48 (module) nil nil ("Issue4260/M.agda" . 1)))
(agda2-highlight-add-annotations 'nil '(72 73 (function) nil nil ("Issue4260.agda" . 72)) '(76 79 (primitive) nil nil ("agda-default-include-path/Agda/Primitive.agda" . 311)) '(82 85 (primitive) nil nil ("agda-default-include-path/Agda/Primitive.agda" . 311)))
(agda2-highlight-add-annotations 'nil '(72 73 (function) nil nil ("Issue4260.agda" . 72)) '(86 87 (function) nil nil ("Issue4260.agda" . 72)) '(88 89 (bound) nil nil ("Issue4260.agda" . 88)) '(90 91 (symbol) t) '(92 93 (postulate) nil nil ("Issue4260/M.agda" . 39)) '(94 95 (bound) nil nil ("Issue4260.agda" . 88)))
(agda2-highlight-add-annotations 'nil '(1 7 (keyword) t) '(8 17 (module) nil nil ("Issue4260.agda" . 1)) '(18 23 (keyword) t))
(agda2-highlight-add-annotations 'nil '(50 70 (comment) t) '(74 75 (symbol) t) '(80 81 (symbol) t))
(agda2-status-action "Checked")
(agda2-info-action "*All Done*" "" nil)
((last . 1) . (agda2-goals-action '()))
